Skip to content

Use simplify_exprtt::resultt in pre-order simplification steps #6118

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
merged 2 commits into from
Nov 8, 2023
Merged

Use simplify_exprtt::resultt in pre-order simplification steps #6118

merged 2 commits into from
Nov 8, 2023

Conversation

@tautschnig
Copy link
Collaborator

The use of resultt increases type safety as the expression to be
simplified is no longer modified in place. All post-order simplification
steps already use resultt, but pre-order steps had been left to be
done.

  • Each commit message has a non-empty body, explaining why the change was made.
  • Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
  • n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
  • Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
  • n/a My commit message includes data points confirming performance improvements (if claimed).
  • My PR is restricted to a single feature or bugfix.
  • n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

@codecov
Copy link

codecov bot commented May 14, 2021 •
edited
Loading

Codecov Report

Attention: 4 lines in your changes are missing coverage. Please review.

Comparison is base (9238a38) 77.75% compared to head (5d29491) 78.94%.

Additional details and impacted files 
@@             Coverage Diff             @@
##           develop    #6118      +/-   ##
===========================================
+ Coverage    77.75%   78.94%   +1.18%     
===========================================
  Files         1701     1701              
  Lines       196465   196502      +37     
===========================================
+ Hits        152762   155120    +2358     
+ Misses       43703    41382    -2321
Files Coverage Δ
src/util/simplify_expr_array.cpp 94.23% <100.00%> (+21.31%) ⬆️
src/util/simplify_expr_class.h 90.47% <ø> (+14.28%) ⬆️
src/util/simplify_expr_pointer.cpp 88.31% <100.00%> (+22.03%) ⬆️
src/util/simplify_expr_struct.cpp 85.36% <100.00%> (+0.24%) ⬆️
src/util/simplify_expr.cpp 86.23% <97.50%> (+13.38%) ⬆️
src/util/simplify_expr_if.cpp 42.77% <93.93%> (+16.86%) ⬆️

... and 87 files with indirect coverage changes

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.

kroening
kroening reviewed Nov 8, 2021
View reviewed changes
src/util/simplify_expr_if.cpp
auto r_truevalue = simplify_rec(swap_branches ? falsevalue : truevalue);
if(swap_branches)
r_truevalue.expr_changed = CHANGED;

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Why is this needed? The if-expression will be marked as changed anyway.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, but build_if_expr would not actually replace the truevalue.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I have refactored the code and added a comment.

kroening
kroening reviewed Nov 8, 2021
View reviewed changes
@tautschnig tautschnig self-assigned this Feb 26, 2022
@tautschnig tautschnig mentioned this pull request May 26, 2022
Closed
4 tasks
@tautschnig tautschnig removed their assignment Oct 24, 2022
@tautschnig tautschnig force-pushed the simplify-resultt branch 2 times, most recently from 947d049 to 18db8ab Compare November 7, 2022 11:24
@tautschnig tautschnig force-pushed the simplify-resultt branch 3 times, most recently from 2d0250e to 337d85b Compare November 20, 2022 21:38
@tautschnig tautschnig mentioned this pull request Nov 28, 2022
Draft
2 tasks
@tautschnig
Use simplify_exprtt::resultt in pre-order simplification steps
183bc7e 
The use of resultt increases type safety as the expression to be
simplified is no longer modified in place. All post-order simplification
steps already use resultt, but pre-order steps had been left to be
done.
@tautschnig
Simplify selected ID_if operands in preorder traversal
5d29491 
This avoids repeatedly visiting already-simplified operands. On the
example from diffblue#7357 this reduces symex time from 1172 seconds to 922
seconds.
@tautschnig tautschnig mentioned this pull request Nov 6, 2023
Open
4 tasks
@tautschnig tautschnig merged commit b836b4f into diffblue:develop Nov 8, 2023
@tautschnig tautschnig deleted the simplify-resultt branch November 8, 2023 12:39
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kroening kroening kroening approved these changes

@martin-cs martin-cs martin-cs approved these changes

@peterschrammel peterschrammel Awaiting requested review from peterschrammel peterschrammel is a code owner

@smowton smowton Awaiting requested review from smowton

Assignees

@kroening kroening

@peterschrammel peterschrammel

Labels

cleanup

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@tautschnig @kroening @martin-cs @peterschrammel